D, D':dsys{i:l}, P:({es:ES{i}| d-es{i:l}(D; es) }Prop{i'}).
d-realizes{i:l}(D; es.P(es))  {d-sub{i:l}(D; D')  d-realizes{i:l}(D'; es.P(es))} 

latex

Definitions	t  T, P  Q, x:A. B(x), D1  D2, Dsys, D realizes es. P(es), Prop, es is an event system of D, ES, x(s), x. t(x), {T}
Lemmas	d-realizes wf, event system wf, d-es wf, dsys wf, d-sub wf, d-sub transitivity